T:Type, L:(T List), R:({x:T| (x  L)} Realizer), B:Realizer.
R-icompat(xL.R(x);B)  (xL. R-icompat(R(x);B)) 

latex

Definitions	A c B, tt, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , R-icompat(A;B), reduce(f;k;as), (L), x. t(x), map(f;as), , Y, P  Q, P  Q, P & Q, xL. P(x), x(s), xL.R(x), P  Q, Realizer, t  T, x:A. B(x), ||as||, x:A. B(x), (x  l)
Lemmas	subtype rel set, l member subtype, l member-set, list-set-type, l all cons, iff functionality wrt iff, all functionality wrt iff, Rall wf, iff wf, Rnone-icompat, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, l all wf2, es realizer wf, Rlist wf, l member wf, R-icompat wf